COMMENT ⊗   VALID 00002 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	
 00003 ENDMK
⊗;

CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[1]∨LENGTH[5];

ELAPSED-TIME =2016

NIL 1 2
1 ¬(cb(m,x)∧(mv(y,x,b)∧(i(y)∧(i(x)∧t(x)))));3 4
2 mv(m,c,b);AXIOM
3 ¬(cb(m,x)∧(t(x)∧u(x,b)));5 6
4 mv(z,x,y)∧(i(z)∧(i(x)∧i(y)))⊃cl(y,f)∨u(x,y);AXIOM
5 ¬(t(x)∧(o(m,x)∧u(x,b)));7 8
6 cb(x,y)⊃o(x,y);AXIOM
7 ¬cl(m,b);9 10
8 t(y)∧(o(x,y)∧u(y,b))⊃cl(x,b);AXIOM
9 ¬r(m,b);THM